Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		x + 0	→ x
2:		x + s(y)	→ s(x + y)
3:		x * 0	→ 0
4:		x * s(y)	→ (x * y) + x
5:		ge(x,0)	→ true
6:		ge(0,s(y))	→ false
7:		ge(s(x),s(y))	→ ge(x,y)
8:		x - 0	→ x
9:		s(x) - s(y)	→ x - y
10:		fact(x)	→ iffact(x,ge(x,s(s(0))))
11:		iffact(x,true)	→ x * fact(x - s(0))
12:		iffact(x,false)	→ s(0)

There are 10 dependency pairs:


13:		x +# s(y)	→ x +# y
14:		x *# s(y)	→ (x * y) +# x
15:		x *# s(y)	→ x *# y
16:		GE(s(x),s(y))	→ GE(x,y)
17:		s(x) -# s(y)	→ x -# y
18:		FACT(x)	→ IFFACT(x,ge(x,s(s(0))))
19:		FACT(x)	→ GE(x,s(s(0)))
20:		IFFACT(x,true)	→ x *# fact(x - s(0))
21:		IFFACT(x,true)	→ FACT(x - s(0))
22:		IFFACT(x,true)	→ x -# s(0)

The approximated dependency graph contains 5 SCCs: {13}, {15}, {17}, {16} and {18,21}.

Consider the SCC {13}. There are no usable rules. By taking the AF π with π(+#) = 2 together with the lexicographic path order with empty precedence, rule 13 is strictly decreasing.

Consider the SCC {15}. There are no usable rules. By taking the AF π with π(*#) = 2 together with the lexicographic path order with empty precedence, rule 15 is strictly decreasing.

Consider the SCC {17}. There are no usable rules. By taking the AF π with π(-#) = 1 together with the lexicographic path order with empty precedence, rule 17 is strictly decreasing.

Consider the SCC {16}. There are no usable rules. By taking the AF π with π(GE) = 1 together with the lexicographic path order with empty precedence, rule 16 is strictly decreasing.

Consider the SCC {18,21}. The usable rules are {5-9}. The constraints could not be solved.

Tyrolean Termination Tool (0.11 seconds) --- May 4, 2006